(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun i () Real)
(declare-fun l () Real)
(declare-fun m () Real)
(declare-fun p () Real)
(assert (forall ((j Real)) (distinct (<= e 0) (distinct (<= j 0) (<= 0 (+ (* a j) c) (+ (* (/ 100 a 0) j)) e)))))
(assert (exists ((k Real)) (=> (and (<= 0 h) (>= 0 h) (= c 1 l) (= d 0 p) (< 0 i)) (< 0 f))))
(assert (= a m))
(assert (= b (mod p g)))
(check-sat)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun i () Real)
(declare-fun l () Real)
(declare-fun m () Real)
(declare-fun p () Real)
(assert (forall ((j Real)) (distinct (<= e 0) (distinct (<= j 0) (<= 0 (+ (* a j) c) (+ (* (/ 100 a 0) j)) e)))))
(assert (exists ((k Real)) (=> (and (<= 0 h) (>= 0 h) (= c 1 l) (= d 0 p) (< 0 i)) (< 0 f))))
(assert (= a m))
(assert (= b (mod p g)))
(check-sat)
